Automating and scaling pre-silicon functional verification of state-of-the-art hardware designs, such as microprocessors and microcontrollers, presents many challenges. These designs employ wide datapaths with arithmetic, logical, and memory units, and complex control logic that coordinates their functionality. The latter typically includes a set of high-level optimizations aimed at increasing a design's throughput, and reducing its area and power consumption. The complexity of both the datapath and control logic results in an enormous state space with vast room for design errors. Furthermore, the progression in the design of hardware systems like microprocessors leads to ever-increasing control logic complexity, and overall chip size, as predicted by Moore's law.
In contrast to simulation, which typically examines a (relatively) small number of scenarios when testing a design, formal verification systematically proves correctness of a design by exhaustively examining the entire design's state space searching for violations to a well-specified behavior. The size of the state space grows exponentially with the size of the design, leading to the so-called state explosion problem. Since the control logic and datapath of contemporary designs are also growing exponentially (in both size and complexity), the formal verification ‘barrier’ grows doubly exponentially, and significantly lags behind the design capability, leading to an exponentially growing verification gap. The increase in complexity and size of today's designs, as well as the difficulty of formally verifying these designs.
Verification thus, cannot be made tractable without a divide-and-conquer approach that tailors different verification methodologies to various parts of the design with different structural patterns. To be effective, these methodologies must be applied at suitable levels of abstraction. In particular, descriptions given at the Register-Transfer Level (RTL) accurately capture the functionality of hardware designs by preserving high-level semantic information that is otherwise lost when moving to the gate- or transistor-level representations. It is, therefore, reasonable to assume that the design under verification be given as an RTL model in a suitable Hardware Description Language (HDL) such as Verilog.
At this level, a reasonable distinction can be made between the datapath and the control logic, and appropriate verification schemes can be applied to each. Datapath units can usually be isolated and verified separately with methods that exploit their structural regularity. Once verified, many datapath elements can be reused across various designs and architectures. Control logic, on the other hand, globally “routes” the flow of data in a design, and thus has to be verified at the level of the entire design. Moreover, control circuitry is invariably custom-made for the architecture and design at hand, precluding the use of previous verification results.
Current verification efforts have tackled control logic verification by generating new mathematical models, typically based on abstraction, that correspond to the RTL description of the design, and utilizing theorem provers to reason about them. Although these models simplify the datapath, they are roughly as complex as the original RTL model. Consequently, hundreds of man-hours are required to manually regenerate the verification model from the RTL model. Moreover, a cumbersome process is required to keep both models consistent, and to prevent subtle bugs from being introduced in the abstract model or masked from the RTL model.
Theorem provers use a number of mathematical approaches to certify that a design complies with its desired functionality, and typically incorporate a number of theories, ranging from zero-, to first-, to higher-order logics, to incrementally prove correctness. In addition to the drawbacks of verifying an abstract model separately from the RTL description, theorem provers are not fully automatic; although equipped with a set of engines on their back-end, the user is required in many cases to guide the power by applying specific engines in the various phases of the proof. In the best case, manual reasoning significantly impedes the verification task for complex designs, and in the average case it makes it completely infeasible. This section provides background information related to the present disclosure which is not necessarily prior art.